\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$,$B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$f$:((?$\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $g$:($\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}$).
\-\\[0ex]combine{-}ecl{-}tuples2($A$; $B$; $f$; $g$) $\in$ ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$)
\end{tabbing}